$\forall$$A$, $B$:Type, $g$:($A$$\rightarrow$($B$ + Top)), $X$:MaInterface($A$). ma{-}interface{-}compose($g$;$X$) $\in$ MaInterface($B$)